home *** CD-ROM | disk | FTP | other *** search
/ Celestin Apprentice 2 / Apprentice-Release2.iso / Tools / Languages / Caml Light 0.61 / Binaries / examples / kb / kb.ml < prev    next >
Encoding:
Text File  |  1993-09-24  |  4.6 KB  |  138 lines  |  [TEXT/ttxt]
  1. #open "prelude";;
  2. #open "terms";;
  3. #open "equation";;
  4.  
  5. (****************** Critical pairs *********************)
  6.  
  7. (* All (u,sig) such that N/u (&var) unifies with M,
  8.    with principal unifier sig *)
  9. (* super : term -> term -> (num list & subst) list *)
  10. let super M = suprec where rec suprec = function
  11.     Term(_,sons) as N ->
  12.       let collate (pairs,n) son =
  13.        (pairs @ map (fun (u,sig) -> (n::u,sig)) (suprec son), n+1) in
  14.       let insides = fst (it_list collate ([],1) sons) in
  15.         begin try
  16.           ([], unify(M,N)) :: insides
  17.         with Failure _ ->
  18.           insides
  19.         end
  20.   | _ -> []
  21. ;;
  22.  
  23. (* Ex :
  24. let (M,_) = <<F(A,B)>> 
  25. and (N,_) = <<H(F(A,x),F(x,y))>> in super M N;;
  26. ==> [[1],[2,Term ("B",[])];                      x <- B
  27.      [2],[2,Term ("A",[]); 1,Term ("B",[])]]     x <- A  y <- B
  28. *)
  29.  
  30. (* All (u,sig), u&[], such that N/u unifies with M *)
  31. (* super_strict : term -> term -> (num list & subst) list *)
  32. let super_strict M = function
  33.       Term(_,sons) ->
  34.         let collate (pairs,n) son =
  35.           (pairs @ map (fun (u,sig) -> (n::u,sig)) (super M son), n+1) in
  36.         fst (it_list collate ([],1) sons)
  37.     | _ -> []
  38. ;;
  39.  
  40. (* Critical pairs of L1=R1 with L2=R2 *)
  41. (* critical_pairs : term_pair -> term_pair -> term_pair list *)
  42. let critical_pairs (L1,R1) (L2,R2) =
  43.   let mk_pair (u,sig) =
  44.      substitute sig (replace L2 u R1), substitute sig R2 in
  45.   map mk_pair (super L1 L2);;
  46.  
  47. (* Strict critical pairs of L1=R1 with L2=R2 *)
  48. (* strict_critical_pairs : term_pair -> term_pair -> term_pair list *)
  49. let strict_critical_pairs (L1,R1) (L2,R2) =
  50.   let mk_pair (u,sig) =
  51.     substitute sig (replace L2 u R1), substitute sig R2 in
  52.   map mk_pair (super_strict L1 L2)
  53. ;;
  54.  
  55. (* All critical pairs of eq1 with eq2 *)
  56. let mutual_critical_pairs eq1 eq2 =
  57.   (strict_critical_pairs eq1 eq2) @ (critical_pairs eq2 eq1);;
  58.  
  59. (* Renaming of variables *)
  60.  
  61. let rename n (t1,t2) =
  62.   let rec ren_rec = function
  63.     Var k -> Var(k+n)
  64.   | Term(op,sons) -> Term(op, map ren_rec sons) in
  65.   (ren_rec t1, ren_rec t2)
  66. ;;
  67.  
  68. (************************ Completion ******************************)
  69.  
  70. let deletion_message (k,_) =
  71.   print_string "Rule ";print_int k; message " deleted"
  72. ;;
  73.  
  74. (* Generate failure message *)
  75. let non_orientable (M,N) =
  76.     pretty_term M; print_string " = "; pretty_term N; print_newline()
  77. ;;
  78.  
  79. (* Improved Knuth-Bendix completion procedure *)
  80.  
  81. let kb_completion greater = kbrec where rec kbrec n rules =
  82.   let normal_form = mrewrite_all rules
  83.   and get_rule k = assoc k rules in process
  84.   where rec process failures = processf
  85.   where rec processf (k,l) =
  86.    (processkl where rec processkl eqs =
  87.      match eqs with
  88.      [] ->
  89.       if k<l then next_criticals (k+1,l) else
  90.       if l<n then next_criticals (1,l+1) else
  91.        (match failures with
  92.           [] -> rules (* successful completion *)
  93.         | _  -> message "Non-orientable equations :";
  94.                 do_list non_orientable failures;
  95.                 failwith "kb_completion")
  96.    | (M,N)::eqs ->
  97.       let M' = normal_form M
  98.       and N' = normal_form N
  99.       and enter_rule(left,right) =
  100.         let new_rule = (n+1, mk_rule left right) in
  101.           pretty_rule new_rule;
  102.           let left_reducible (_,(_,(L,_))) = reducible left L in
  103.           let redl,irredl = partition left_reducible rules in
  104.             do_list deletion_message redl;
  105.             let irreds = (map right_reduce irredl
  106.                  where right_reduce (m,(_,(L,R))) = 
  107.                        m,mk_rule L (mrewrite_all (new_rule::rules) R))
  108.             and eqs' = map (fun (_,(_,pair)) -> pair) redl in
  109.              kbrec (n+1) (new_rule::irreds) [] (k,l) (eqs @ eqs' @ failures) in
  110.       if M'=N' then processkl eqs else
  111.       if greater(M',N') then enter_rule(M',N') else
  112.       if greater(N',M') then enter_rule(N',M') else
  113.         process ((M',N')::failures) (k,l) eqs)
  114.   and next_criticals (k,l) =
  115.     try
  116.       let (v,el) = get_rule l in
  117.         if k=l then
  118.           processf (k,l) (strict_critical_pairs el (rename v el))
  119.         else
  120.           try
  121.             let (_,ek) = get_rule k in 
  122.               processf (k,l) (mutual_critical_pairs el (rename v ek))
  123.       with Not_found (*rule k deleted*) -> next_criticals (k+1,l)
  124.     with Not_found (*rule l deleted*) -> next_criticals (1,l+1)
  125. ;;
  126.  
  127. (* complete_rules is assumed locally confluent, and checked Noetherian with
  128.   ordering greater, rules is any list of rules *)
  129.  
  130. let kb_complete greater complete_rules rules =
  131.     let n = check_rules complete_rules
  132.     and eqs = map (fun (_,(_,pair)) -> pair) rules in
  133.     let completed_rules =
  134.       kb_completion greater n complete_rules [] (n,n) eqs in
  135.     message "Canonical set found :";
  136.     pretty_rules (rev completed_rules);()
  137. ;;
  138.